Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    fib(N)  → sel(N,fib1(s(0),s(0)))
2:    fib1(X,Y)  → cons(X,n__fib1(Y,n__add(X,Y)))
3:    add(0,X)  → X
4:    add(s(X),Y)  → s(add(X,Y))
5:    sel(0,cons(X,XS))  → X
6:    sel(s(N),cons(X,XS))  → sel(N,activate(XS))
7:    fib1(X1,X2)  → n__fib1(X1,X2)
8:    add(X1,X2)  → n__add(X1,X2)
9:    activate(n__fib1(X1,X2))  → fib1(activate(X1),activate(X2))
10:    activate(n__add(X1,X2))  → add(activate(X1),activate(X2))
11:    activate(X)  → X
There are 11 dependency pairs:
12:    FIB(N)  → SEL(N,fib1(s(0),s(0)))
13:    FIB(N)  → FIB1(s(0),s(0))
14:    ADD(s(X),Y)  → ADD(X,Y)
15:    SEL(s(N),cons(X,XS))  → SEL(N,activate(XS))
16:    SEL(s(N),cons(X,XS))  → ACTIVATE(XS)
17:    ACTIVATE(n__fib1(X1,X2))  → FIB1(activate(X1),activate(X2))
18:    ACTIVATE(n__fib1(X1,X2))  → ACTIVATE(X1)
19:    ACTIVATE(n__fib1(X1,X2))  → ACTIVATE(X2)
20:    ACTIVATE(n__add(X1,X2))  → ADD(activate(X1),activate(X2))
21:    ACTIVATE(n__add(X1,X2))  → ACTIVATE(X1)
22:    ACTIVATE(n__add(X1,X2))  → ACTIVATE(X2)
The approximated dependency graph contains 3 SCCs: {14}, {18,19,21,22} and {15}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.23 seconds)   ---  May 3, 2006